Орнаменты

На меня снизошел очередной микро-инсайт-просветление и я сразу же спешу с вами
ним поделиться. Абсоюлтно очевидная и прекрасная вещь. Признаюсь честно, что я
в глаза формулировок не видел, но вот система сразу нарисовалась перед глазами.
Кто читал МакБрайда поправит меня, я уверен.

Как вы знаете, все конструкторы (ко)-индуктивных типов могут состоять из
параметров и типа результата конструктора. Последний может и не находиться во
вселенной этого типа, а быть типом Path. Так вот параметры этого типа могут
быть всего трех видов:

1) Unit, как в типе Lazy A: () -> A или ленивом Nil: () -> List A.
2) Fixed Type как в типе первого параметра коснтруктора Cons: A -> List A -> List A.
3) Recursive Type, как в типе второго параметра tail конструктора Cons, или
второго поля tail рекорда коиндуктивного Stream (они равны в MLTT).

Это называется три орнамента. Они все задаются разными профункторами P_{1,2,3},
которые описаны у Паши в блоге. Из этих орнаментов мы конструируем тела термов
в наших кодировках (всех их модификациях). Круто да? Это еще не все, суть
орнаментов не в этом, а в том что вы можете транзакционно добавлять новые
параметры в существующие конструкторы. В современных пруверах и в ООП в
операции extend применимое к структурам или рекордам действует на уровне
добавления новых конструкторов только, а не модификации (версионировании)
существующих. Орнаменты же позволяют делать версионирование типовых интерфейсов
и структур, и позволяют избежать случает когда приходится называть линковочные
интерфейсы DirectDraw2. С помощью орнаментов вы можете добавлять аргументы в
существующие конструкторы или менят их тип. Я привел только три орнамента,
которых достаточно чтобы покрыть все существующие базовые библиотеки всех
языков программирования :-) А представьте что орнаментов может быть больше!

Представьте себе аморфную и текущую структуру которую меняет свою систему типов
автоматичеки подстариваясь по нужную реальность. И при этом вы видете историю
всех трейсов измениений транзакционного лога каждого типа. В этом логе типа с
одним и тем же именем могут рождаться и умирать, но вы при этом всегда будете
знать с скем линковаться, так как в типах будет присуствовать время его версии
и диапазон совместимости.

Как вам такой "внутренний лисп" пространства типов?
_______________
[1]. https://personal.cis.strath.ac.uk/conor.mcbride/pub/OAAO/LitOrn.pdf